- Add while loop syntax to grammar with invariant clauses
- Add parser for while loops (combines multiple invariants with &&)
- Add While case to LaurelToCoreTranslator
- Add leftassoc to arithmetic/logical operators (fixes a * b / c parsing)
- Create T4_WhileBasic.lean test

- Change Procedure.precondition to preconditions : List StmtExpr
- Change Body.Opaque/Abstract postcondition to postconditions : List StmtExpr
- Update grammar: requires/ensures now use Seq instead of Option
- Update parser to collect list of requires/ensures clauses
- Update translator to generate indexed labels (proc_pre_0, proc_post_0, etc.)
- Update LaurelFormat, LaurelEval for list-based contracts
- Update canBeBoogieFunction to check preconditions.isEmpty

- Add constrainedType grammar rule and parser
- Add topLevelConstrainedType to TopLevel
- Build ConstrainedTypeMap from program type definitions
- Resolve constrained types to base types in parameter translation
- Generate constraint checks as preconditions for input parameters
- Generate constraint checks as postconditions for output parameters
- Use resolved types in type environment for expression translation
- Create T10_ConstrainedTypes.lean test

- Thread ctMap through translateStmt
- Resolve constrained types to base types for locals
- Generate assertion after init for constrained type locals

- Thread ctMap through translateExpr and lookupType
- Generate constraint assertion after assignment to constrained type variable

- Handle StaticCall specially in Assign case
- Generate call statement instead of function application

- genConstraintAssert: generates constraint assertion for a variable
- defaultExprForType: generates default value for a type
- isHeapFunction: checks if function is heapRead/heapStore

- Grammar: forallExpr, existsExpr with (name: type) => body syntax
- Parser: translate to Laurel.Forall/Exists AST nodes
- Translator: varCloseByName helper, translate to Core quant expressions
- Test: T5_Quantifiers.lean

- forall(x: nat) => body becomes forall x. (x >= 0) ==> body
- exists(x: nat) => body becomes exists x. (x >= 0) && body
- Made translateExpr partial to allow recursive constraint translation

- Add TranslatedConstraintMap with pre-translated Core constraint expressions
- Add translateSimpleExpr for constraint expressions (no quantifiers)
- Build tcMap upfront in translate(), pass through all functions
- Quantifiers use pre-translated constraints, avoiding recursive call on external data
- Restore termination proof for translateExpr

- Explicit cases for Forall/Exists with clear error message
- Better error messages for unsupported operators

Reduces duplication between translateExpr and translateSimpleExpr

- Array type translates to Map int elemType
- Array.Get uses select operation (Core infers types)
- Array.Length uses name#len free variable
- expandArrayParam expands array params to (arr, arr#len) pairs
- Fixed CoreIdent visibility: use unres for operations, matching factory convention

- Sequences represented as (arr, start, end) bounds
- Seq.Contains translates to existential: exists i :: start <= i < end && arr[i] == elem
- Seq.Take adjusts end bound
- Seq.Drop adjusts start bound
- No new axioms needed - direct translation to quantifiers
- Fixed identifier matching for guillemet-escaped names («Seq.Contains» etc)

- Add Forall and Exists cases to isPureExpr so pure functions with
  quantifiers can be translated as Core functions (fixes non-termination)
- Map 'Map' type to SMT 'Array' type in both lMonoTyToSMTString and
  encodeType

Note: There's a remaining issue with user-defined functions taking Map
arguments when called in while loop invariants - the UF key mismatch
between definition and call sites needs further investigation.

…lation

This adds a FunctionTypeMap that maps function names to their types,
built from procedures that can be translated as functions. When
translating a StaticCall, we look up the function type and attach it
to the .op expression.

This is necessary for the SMT encoder to correctly encode user-defined
function calls, as it needs the type information to create the correct
uninterpreted function signatures.

Note: There is still an issue where the type annotation is lost during
evaluation. The type is present in the translated Core program but
missing in the VCs. This needs further investigation.

Grammar:
- Add spacing around operators for readable output
- Add divT, modT (truncating division) and implies operators
- Use NewlineSepBy + indent() for block formatting
- Add newline prefixes for requires/ensures/invariant clauses
- Fix call precedence for proper parsing

Translator:
- Replace panic! with Except String for proper error handling
- Add expandArrayArgs and injectQuantifierConstraint helpers
- Add normalizeCallee for «» quoted identifiers
- Validate array types in Seq.From
- Support multiple invariants (combined with &&)

CLI:
- Add laurelParse, laurelAnalyze, laurelToCore, laurelPrint commands

Tests:
- Add testTruncatingDiv, testUnary, implies tests
- Add multiContract for multiple requires/ensures